% 
% <<<<<<< .mine
% In this section we formalize the dynamics of reaction systems with response time (\rsd) through Petri nets with timestamps.
% We are given a set \res of species ranged over $R, S$. 
% The status of the species solely depends on a measure, called the \emph{decay time}, defining its period of availability in the system for efficiently triggering or inhibiting reactions: a species is \emph{available} whenever its decay time has not expired otherwise it is \emph{unavailable}.
% The function $\life:\res \to \nat$ provides the decay time for each species. 
% ======= 
In this section we describe the principles of the dynamics of reaction systems with duration (\rsd) and we formalize them through Petri nets with timestamps.

We are given a set \res of species, where each species is associated to a \emph{decay time} defined by a function $\life:\res \to \nat$, that represents its period of availability in the system. Thus, we say that a species is \emph{available} if its decay time has not run out otherwise it is \emph{unavailable}. 

The evolution of species is governed by reactions. A reaction system \RS is a set of reactions of the form $(R, I, P) \subseteq (\res \times \res \times \res)$ where $R$ is the set of reactants, $I$ the set of inhibitors and $P$ the set of products. Similarly as for species, to each reaction we associate  a measure,    the \emph{response time} (a function $\dur: \RS \to \nat$),  that characterizes the time required for yielding a product.  A reaction $r$ is \emph{enabled} if and only if all the reactants are available and all the inhibitors are unavailable during the whole response time period $\dur(r)$. The triggering of a reaction results in the production of some species. More precisely, if a species $S$ was unavailable before triggering the reaction it will be present afterwards. Otherwise, if it was already present, it will be \emph{refreshed}, that is a new cycle of decay is started. 

The dynamics of the system relies on the production and degradation of species. Essentially, this  is based on the evolution of species status:  from available to unavailable and vice versa. Moreover, the system is initialized with a set of available species $\res_0$ ($\subseteq \res$) with their full decay time.


In order to formalize  the evolution of species and reaction triggering,  we use \emph{timestamps} that record the switch of status. 
Hence, we will represent species as triples $\tuple{\bool, \refr, \birth}$: $\bool$ is a boolean value storing  the status:  unavailable $0$ or available $1$; $\refr$ is a timestamp recording the last date of refresh: if the species is unavailable we assign $\refr =0$; and $\birth$ is the timestamp that logs the last date when status changed. %Notice that field $\refr$ has no particular meaning when the species is unavailable.
According to this representation:
\begin{itemize}
 \item All the timestamps updates are referred to a unique global clock. 
 
\item In the initial configuration, all species in $\res_0$ are set to $\tuple{1, 0, 0}$ and all others in $\res \setminus \res_0$ to $\tuple{0, 0, 0}$.

\item As time passes by, available resources that are not sustained by a reaction, decay. When their decay time is elapsed they become unavailable, leading to set: boolean $\bool$ to 0, $\birth$ to the actual value of the clock and $\refr$ to 0. 


\item The refresh process resulting from a reaction is defined as follows: if the species was available ($\bool=1$), the field $\refr$ is updated to the current value of the clock. Otherwise, if the species was unavailable ($\bool=0$), its status $\bool$ is switched from $0$ to $1$ and fields $\refr$ and $\birth$ are set to the current value of the clock. 
\end{itemize}

It is worth noticing that if a species is continuously sustained  by some reactions then it remains available in the system for a period that could be longer than its decay time. This is witnessed by the fact that the values of fields $\birth$ and $\refr$ can be different: the first representing the starting date of availability and the second 
 the last date of refresh. 

 

\subsection{Petri net with timestamps}

We now present the formalization of \rsd into an instance of Petri nets with causal time that we call \emph{Petri nets with timestamps}. For a more complete introduction on Petri nets with causal time see \cite{DBLP:journals/entcs/ThanhKP02}.  Given a set of variables  ranged over $x, y, z, \dots$, Petri nets with timestamps are defined as follows:
%%ranging over $x, y$ \dots

\begin{definition}[Petri net with timestamps]\label{def:PTS}
A \emph{Petri Net with timestamps} $TS$ is a tuple $(Q, T, F, L, m_0)$ where:
\begin{itemize}
 \item $Q$ is the set of places, among those we identify a special place called $\Pclock$ (the clock);
 \item $T$ is the set of transitions and $Q \cap T = \emptyset$;
 \item $F: T \to 2^Q \times 2^Q$ is the transition function associating to each transition $t$ two set of places called the pre-set ($^{\bullet}t$) and the post-set ($t^{\bullet}$) of $t$;

 \item $L$ is a labeling function from $ Q \cup T \cup (Q \times T) \cup (T \times Q) $ to a set of labels defined as follows:

\underline{Labels for places}: 
$$
 L: \begin{cases}
\Pclock \to \nat \\
 Q \setminus \{\Pclock \} \to \{0,1 \} \times \nat \times \nat 
   \end{cases}
$$
\underline{Labels for transitions}: 
$$
 L: T \to BE(V, \nat)
$$
they represent guarding function from $T$ to boolean expressions $BE()$ on $V$ and $\nat$.\\
\underline{Labels for arcs}:
$$
 L: (Q\times T) \cup (T \times Q) \to (V \cup \nat)\cup (V \cup \{0,1 \}) \times (V \cup \nat) \times (V \cup \nat);
$$

\item $m_0$ is the initial marking.
\end{itemize} 

 We define the marking function $M: Q \to \nat \cup (\{0,1\} \times \nat \times \nat)$ so that $M(\Pclock) \in \nat$ and $\forall q \in Q \setminus \{\Pclock\}$ $M(q) \in \{0,1\} \times \nat \times \nat$.

A transition $t \in T$ is \emph{enabled} if there exists an evaluation $\rho$ of all the variables in the labeling of input and output arcs such that 
\begin{itemize}
 \item $L_{\rho}(t) = \mathsf{true}$, 
 \item $\forall q \in \pre{t}$ $L_{\rho}(q,t) = M(q)$
\end{itemize}
 and the firing ($\firing{m}{t}{m'}$) produces the marking: 
\begin{itemize}
 \item $\forall q \in \post{t} \cap \pre{t}$ $M'(q) = L_{\rho}(t,q) -L_{\rho}(q,t) + M(q)$, 
\item and $\forall q \in \post{t} \setminus \pre{t}$ $M'(q) = L_{\rho}(t,q) + M(q)$. 
\end{itemize}
We denote with $\rightarrow^*$ the reflexive and transitive closure of $\rightarrow$.
\end{definition}

Next, we implement the dynamics of \rsd into Petri nets with timestamps.
Thus, we need to encode time, species and reactions. Every  system has one (and only one) clock that counts time, realized by the special place $\Pclock$ and by a transition $t_c$ that represents its evolution (Figure \ref{fig:clock}). Every species in $\res$ is encoded with a corresponding place, and every reaction $r$ corresponds to a transition $t_r$ (Figure \ref{fig:reaction}). More detailed explanations of the implementation follow %An intuition on the guarding functions of transitions is given after 
Definition \ref{def:rs}.
 
\begin{definition}[\rsd net]\label{def:rs}
 Given a set of species $\res$ with associated decay time $\life: \res \to \nat$, an initial set of entities $\res_0 \subseteq \res$ and a \rsd $\RS=\{r_j=(R_j, I_j, P_j)\}_j$ with response time $\dur: \RS \to \nat$, its encoding into Petri nets with timestamps is defined as the tuple $(Q, T,F, L, m_0)$ where:
\begin{itemize}
 \item $Q = \{\Pclock\} \cup \res; $
 \item $T= \{t_c \} \cup \{t_{r} \mid r \in \RS \}$;

 \item $F$ such that:
 $$
\begin{array}{ll}
 \pre{t_c} = \post{t_c}= Q \\

\pre{t_{r}} = \post{t_{r}}=R \cup I \cup P \cup \{\Pclock\} & \forall r = (R,I,P) \in \RS;
\end{array}
 $$

 \item Labels for Places: 
$$
\begin{array}{ll}

L(\Pclock)  \in \nat \\
 L(S_i) \in \{0,1 \} \times \nat \times \nat & \text{for } S_i \in \res;
\end{array}
$$

\item Labels for Transitions:
 $$
\begin{array}{lcl}
 L(t_c) \!&= & \bigwedge_{S_i \in \res} C_i \wedge (z'=z+1) \text{ where }\\
 C_i   &= & \big [ (\bool_i = 1 \wedge z-\refr_i \leq \life(S_i) \wedge \bool_i' = \bool_i \wedge \refr_i'=\refr_i \wedge \birth_i'=\birth_i) \, \vee \\
  &&\ (\bool_i = 1 \wedge z-\refr_i > \life(S_i) \wedge \bool_i' = 0 \wedge \refr_i'=0 \wedge \birth_i'=z') \, \vee \\
  &&\ (\bool_i = 0 \wedge \bool_i' = \bool_i \wedge \refr_i'=\refr_i \wedge \birth_i'=\birth_i)\big]\\ \\

 L(t_r) \! &=& \bigwedge_{S_i \in (R \cup I)}(z-\birth_i \geq \dur(r)) \ \wedge \\
&& \bigwedge_{P_k \in P}\big [ (\bool_k=0 \wedge \birth_k' = z) \vee (\bool_k=1 \wedge \birth_k' = \birth_k) \big] 
\end{array}
 $$
for each $r=(R,I,P) \in \RS$;

\item Labels for Arcs:
$$
\begin{array}{cllc}
t_c & L(\Pclock, t_c) = z & L(t_c, \Pclock ) = z'\\
   & L(S_i, t_c) = \tuple{\bool_i, \refr_i, \birth_i} & L(t_c, S_i) = \tuple{\bool_i', \refr_i', \birth_i'} & \forall S_i\in \res \\ \\

t_r & L(\Pclock, t_r) = z & L(t_r, \Pclock ) = z\\
   & L(R_i,t_r) = \tuple{1, \refr_i, \birth_i} & L(t_r, R_i) = \tuple{1, \refr_i, \birth_i} & \forall R_i \in R \\

   & L(I_j,t_r) = \tuple{0, 0, \birth_j} & L(t_r, I_j) = \tuple{0, 0, \birth_j} & \forall I_j \in I \\

   & L(P_k,t_r) = \tuple{\bool_k, \refr_k, \birth_k} & L(t_r, P_j) = \tuple{1, z, \birth_k'} & \forall P_k \in P 
\end{array}
$$
for each $r=(R,I,P) \in \RS$; 
 

\item The initial marking $m_0$:
$$
m_0(q) =
\begin{cases}
 0 & \text{if } q = \Pclock \\
 \tuple{1,0,0}& \text{if } q \in \res_0\\
 \tuple{0,0,0}& \text{otherwise.}
\end{cases}
$$
\end{itemize}

\end{definition}



We now comment on the transitions of the Petri net. The result of the firing of a transition is handled by  guards (namely $L(t_c)$ and $L(t_r)$) together with the evaluation $\rho$ as described in Definition \ref{def:PTS}.  


For what concerns  clock transition $t_c$, every time the guard $L(t_c)$ is satisfied the clock is incremented by one ($z'=z+1$).  Moreover, $L(t_c)$ handles the conditions of availability of species. If a species $S_i$ is available ($\bool_i=1$) and 
its last refresh has occurred more than $\life(S_i)$ time units ago when compared to the current value $z$ of the clock ($z-\refr_i > \life(S_i)$) then its status become unavailable ($\bool_i'=0, \refr_i'=0$ and $\birth_i'=z'$).
Otherwise, the content of place $S_i$ remains unchanged. 
Notice, that this way the degeneration happens as soon as the entity has exceeded its decay time.


\begin{figure}[t]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 \tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]


  \node [place, label = above: $\Pclock$] (Pc){};
 
 \node [place, below left of= Pc, node distance = 4cm, label=above:$S_i$] (R){};

  \node [transition] (tC) [ right of=R, node distance = 2.8cm, label={[red] right:$L(t_{c})$}] {$t_{c}$}
   edge [pre]    node[right] {$z$}    (Pc)
   edge [post,bend right]   node[right]{$z'$}    (Pc)
   edge [pre, bend right]    node[above] {$\tuple{\bool_i,\refr_i,\birth_i}$}    (R)
   edge [post, bend left]    node[auto] {$\tuple{\bool_i',\refr_i',\birth_i'}$}    (R);
  
\end{tikzpicture}
\caption{Transition for the clock} \label{fig:clock}
\end{figure}

\begin{figure}[t]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 \tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]



 \node [place, label = right: $P$] at (3,0) (P){};
 \node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = above: $R$] at (2,4) (R){};
 \node [place, label = above: $I$] at (4,4) (I){};
 
 \node [transition, label={[red] right:$L(t_{r})$}] at (3,2) (tr) {$t_{r}$}
   edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[left] {$\tuple{1,\refr_i,\birth_i}$}   (R)
   edge [pre and post]    node[right] {$\tuple{0,0,\birth_k}$}     (I)
   edge [pre, bend right]    node[left] {$\tuple{\bool_k,\refr_k,\birth_k}$}   (P)
   edge [post, bend left]   node[right] {$\tuple{1,z,\birth_k'}$}     (P);
  
\end{tikzpicture}
\caption{Transition for a reaction $r= (R, I, P)$} \label{fig:reaction}
\end{figure}

Next, we move to describe transitions for reactions: namely given a reaction $r=(R,I,P)$ we detail the conditions and the results of firing  $t_r$. First, the firing of the transition depends on the availability of reactants in $R$ ($\bool_i =1$) and on the unavailability of inhibitors ($\bool_j =0$). The rest of the constraints are handled by  guard $L(t_r)$. More in detail: we first require that all reactants (resp. inhibitors) have been available (resp. unavailable) for at least $\dur(r)$ time units ($z-\birth_i \geq \dur(r)$) and then we deal with the refresh operation on products. Thus, if the product $P_k$ was unavailable ($\bool_k=0$), we change its status by setting both $\refr_k'$ and $\birth_k'$  to the current value of the clock $z$, otherwise, if it was available, we just refresh its $\refr_k'$ field ($\bool_k=1 \wedge \birth_k' = \birth_k$).
